Termination Proof Script

Consider the TRS R consisting of the rewrite rules
1:    p(0)  → 0
2:    p(s(X))  → X
3:    leq(0,Y)  → true
4:    leq(s(X),0)  → false
5:    leq(s(X),s(Y))  → leq(X,Y)
6:    if(true,X,Y)  → activate(X)
7:    if(false,X,Y)  → activate(Y)
8:    diff(X,Y)  → if(leq(X,Y),n__0,n__s(diff(p(X),Y)))
9:    0  → n__0
10:    s(X)  → n__s(X)
11:    activate(n__0)  → 0
12:    activate(n__s(X))  → s(X)
13:    activate(X)  → X
There are 9 dependency pairs:
14:    LEQ(s(X),s(Y))  → LEQ(X,Y)
15:    IF(true,X,Y)  → ACTIVATE(X)
16:    IF(false,X,Y)  → ACTIVATE(Y)
17:    DIFF(X,Y)  → IF(leq(X,Y),n__0,n__s(diff(p(X),Y)))
18:    DIFF(X,Y)  → LEQ(X,Y)
19:    DIFF(X,Y)  → DIFF(p(X),Y)
20:    DIFF(X,Y)  → P(X)
21:    ACTIVATE(n__0)  → 0#
22:    ACTIVATE(n__s(X))  → S(X)
The approximated dependency graph contains 2 SCCs: {14} and {19}.
Tyrolean Termination Tool  (0.01 seconds)   ---  May 4, 2006